Nuprl Lemma : random-seq_wf
0,22
postcript
pdf
T
:Type,
sz
:
,
eq
:(
T
T
),
f
:(
T
). random-seq(
T
;
sz
;
eq
;
f
)
Prop
latex
Definitions
Type
,
t
T
,
,
,
x
:
A
B
(
x
)
,
,
#$n
,
a
<
b
,
Void
,
P
Q
,
False
,
A
,
A
B
,
,
{
x
:
A
|
B
(
x
) }
,
x
:
A
.
B
(
x
)
,
exp(
i
;
n
)
,
{
i
..
j
}
,
<
a
,
b
>
,
derived-seq(
f
;
s
)
,
eq_seq(
eq
)
,
x
:
A
B
(
x
)
,
frequency(
f
;
x
) ~ (
p
/
q
)
,
S
T
,
S
T
,
increasing(
f
;
k
)
,
Prop
,
random-seq(
T
;
sz
;
eq
;
f
)
Lemmas
increasing
wf
,
frequency
wf
,
eq
seq
wf
,
derived-seq
wf
,
int
seg
wf
,
exp
wf
,
nat
wf
,
bool
wf
,
nat
plus
wf
origin
T:Type, sz:
, eq:(T
T
), f:(T). random-seq(T;sz;eq;f) 
Prop T:Type, sz:, eq:(TT), f:(T). random-seq(T;sz;eq;f) Prop TB(x)
Q
A
B
x:A. B(x)
}
B(x)
T
T